Nuprl Lemma : s-filter_wf
0,22
postcript
pdf
T
:Type,
as
:
T
List,
P
:({
a
:
T
| (
a
as
) }
).
T
s-filter(
P
;
as
)
T
List
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
P
Q
,
s-insert(
x
;
l
)
,
if
b
t
else
f
fi
,
reduce(
f
;
k
;
as
)
,
s-filter(
p
;
as
)
,
Lemmas
bool
wf
,
list-subtype
,
reduce
wf
,
ifthenelse
wf
,
s-insert
wf
,
l
member
wf
origin
T:Type, as:T List, P:({a:T| (a 
as) }
). T 
s-filter(P;as) T List T:Type, as:T List, P:({a:T| (a as) }). T s-filter(P;as) T List Tx:A. B(x) l) Q
t else f fi